/-
Copyright (c) 2025 Amelia Livingston. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Amelia Livingston
-/
module

public import Mathlib.Algebra.Homology.AlternatingConst
public import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
public import Mathlib.CategoryTheory.Preadditive.Projective.Resolution
public import Mathlib.GroupTheory.OrderOfElement
public import Mathlib.RepresentationTheory.Coinvariants

/-!
# Projective resolution of `k` as a trivial `k`-linear representation of a finite cyclic group

Let `k` be a commutative ring and `G` a finite commutative group. Given `g : G` and `A : Rep k G`,
we can define a periodic chain complex in `Rep k G` given by
`... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0`
where `N` is the norm map sending `a : A` to `∑ ρ(g)(a)` for all `g` in `G`.

When `G` is generated by `g` and `A` is the left regular representation `k[G]`, this chain complex
is a projective resolution of `k` as a trivial representation, which we prove here.

In the file `Mathlib/RepresentationTheory/Homological/GroupHomology/FiniteCyclic.lean`, we use
this resolution to compute the group homology of representations of finite cyclic groups.

## Main definitions

* `Rep.FiniteCyclicGroup.resolution k g hg`: given a finite cyclic group `G` generated by `g : G`,
  this is the projective resolution of `k` as a trivial `k`-linear `G`-representation given by
  periodic complex
  `... ⟶ k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] ⟶ 0` where `ρ` is
  the left regular representation and `N` is the norm map.

## TODO

* Use this to analyse the group cohomology of representations of finite cyclic groups.

-/

@[expose] public section

universe v u

open CategoryTheory Finsupp

namespace Representation.FiniteCyclicGroup

variable {k G V : Type*} [CommRing k] [Group G] [Fintype G] {V : Type*} [AddCommGroup V]
  [Module k V] (ρ : Representation k G V) (g : G)

lemma coinvariantsKer_eq_range (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    Coinvariants.ker ρ = LinearMap.range (ρ g - LinearMap.id) := by
  refine le_antisymm (Submodule.span_le.2 ?_) ?_
  · rintro a ⟨⟨γ, α⟩, rfl⟩
    rcases mem_powers_iff_mem_zpowers.2 (hg γ) with ⟨i, rfl⟩
    induction i with | zero => exact ⟨0, by simp⟩ | succ n _ =>
    use (Fin.partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) α) (Fin.last _))
    simpa using ρ.apply_sub_id_partialSum_eq _ _ _
  · rintro x ⟨y, rfl⟩
    simpa using Coinvariants.sub_mem_ker g y

/-- Given a finite cyclic group `G` generated by `g` and a `G` representation `(V, ρ)`, `V_G` is
isomorphic to `V ⧸ Im(ρ(g - 1))`. -/
noncomputable def coinvariantsEquiv (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    ρ.Coinvariants ≃ₗ[k] (_ ⧸ LinearMap.range (ρ g - LinearMap.id)) :=
  Submodule.quotEquivOfEq _ _ (coinvariantsKer_eq_range ρ g hg)

lemma coinvariantsKer_leftRegular_eq_ker :
    Coinvariants.ker (Representation.leftRegular k G) =
      LinearMap.ker (linearCombination k (fun _ => (1 : k))) := by
  refine le_antisymm (Submodule.span_le.2 ?_) fun x hx => ?_
  · rintro x ⟨⟨g, y⟩, rfl⟩
    simpa [linearCombination, sub_eq_zero, sum_fintype]
      using Finset.sum_bijective _ (Group.mulLeft_bijective g⁻¹) (by aesop) (by aesop)
  · have : x = x.sum (fun g r => single g r - single 1 r) := by
      ext g
      by_cases hg : g = 1
      · simp_all [linearCombination, sum_apply']
      · simp_all [sum_apply']
    rw [this]
    exact Submodule.finsuppSum_mem _ _ _ _ fun g _ =>
      Coinvariants.mem_ker_of_eq g (single 1 (x g)) _ (by simp)

end Representation.FiniteCyclicGroup

namespace Rep.FiniteCyclicGroup

variable (k : Type u) {G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G)

namespace leftRegular

open Finsupp IsCyclic Representation

lemma range_norm_eq_ker_applyAsHom_sub (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    LinearMap.range (leftRegular k G).norm.hom.hom =
      LinearMap.ker (applyAsHom (leftRegular k G) g - 𝟙 _).hom.hom :=
  le_antisymm (fun _ ⟨_, h⟩ => by simp_all [← h]) fun x hx => ⟨single 1 (x g), by
    ext j; simpa [Representation.norm] using (apply_eq_of_leftRegular_eq_of_generator g hg _
      (by simpa [sub_eq_zero] using hx) j).symm⟩

lemma range_applyAsHom_sub_eq_ker_linearCombination (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    LinearMap.range (applyAsHom (leftRegular k G) g - 𝟙 _).hom.hom =
      LinearMap.ker (linearCombination k (fun _ => (1 : k))) := by
  simp [← FiniteCyclicGroup.coinvariantsKer_eq_range _ _ hg,
    ← FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker]

lemma range_applyAsHom_sub_eq_ker_norm (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    LinearMap.range (applyAsHom (leftRegular k G) g - 𝟙 _).hom.hom =
      LinearMap.ker (leftRegular k G).norm.hom.hom := by
  simp [ker_leftRegular_norm_eq, ← range_applyAsHom_sub_eq_ker_linearCombination k g hg]

end leftRegular

/-- Given a finite group `G` and `g : G`, this is the functor `Rep k G ⥤ ChainComplex (Rep k G) ℕ`
sending `A : Rep k G` to the periodic chain complex in `Rep k G` given by
`... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0`
where `N` is the norm map. When `G` is generated by `g` and `A` is the left regular representation
`k[G]`, it is a projective resolution of `k` as a trivial representation.

It sends a morphism `f : A ⟶ B` to the chain morphism defined by `f` in every degree. -/
@[simps]
noncomputable def chainComplexFunctor : Rep k G ⥤ ChainComplex (Rep k G) ℕ where
  obj A := HomologicalComplex.alternatingConst A (φ := A.norm) (ψ := applyAsHom A g - 𝟙 A)
    (by ext; simp) (by ext; simp) fun _ _ => ComplexShape.down_nat_odd_add
  map f := {
    f i := f
    comm' := by
      rintro i j ⟨rfl⟩
      by_cases hj : Even (j + 1)
      · simp [if_pos hj, norm_comm]
      · simp [if_neg hj, applyAsHom_comm] }
  map_id _ := rfl
  map_comp _ _ := rfl

variable {k}

/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
this is the short complex in `ModuleCat k` given by `A --N--> A --(ρ(g) - 𝟙)--> A`
where `N` is the norm map. Its homology is `Hⁱ(G, A)` for even `i` and `Hᵢ(G, A)` for odd `i`. -/
noncomputable abbrev normHomCompSub : ShortComplex (ModuleCat k) :=
  ShortComplex.mk A.norm.hom (applyAsHom A g - 𝟙 A).hom (by ext; simp)

/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
this is the short complex in `ModuleCat k` given by `A --N--> A --(ρ(g) - 𝟙)--> A`
where `N` is the norm map. Its homology is `Hⁱ(G, A)` for even `i` and `Hᵢ(G, A)` for odd `i`. -/
noncomputable abbrev subCompNormHom : ShortComplex (ModuleCat k) :=
  ShortComplex.mk (applyAsHom A g - 𝟙 A).hom A.norm.hom (by ext; simp)

/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
this is the periodic chain complex in `ModuleCat k` given by
`... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0` where `N` is the norm map.
Its homology is the group homology of `A`. -/
noncomputable abbrev moduleCatChainComplex : ChainComplex (ModuleCat k) ℕ :=
  HomologicalComplex.alternatingConst A.V (φ := A.norm.hom) (ψ := (applyAsHom A g - 𝟙 A).hom)
    (by ext; simp) (by ext; simp) fun _ _ => ComplexShape.down_nat_odd_add

/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
this is the periodic chain complex in `Rep k G` given by
`0 ⟶ A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A --N--> A ⟶ ...` where `N` is the norm map.
Its cohomology is the group cohomology of `A`. -/
noncomputable abbrev moduleCatCochainComplex : CochainComplex (ModuleCat k) ℕ :=
  HomologicalComplex.alternatingConst A.V (φ := (applyAsHom A g - 𝟙 A).hom) (ψ := A.norm.hom)
    (by ext; simp) (by ext; simp) fun _ _ => ComplexShape.up_nat_odd_add

variable (k)

/-- Given a finite cyclic group `G` generated by `g : G`, let `P` denote the periodic chain complex
of `k`-linear `G`-representations given by
`... ⟶ k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] ⟶ 0` where `ρ` is
the left regular representation and `N` is the norm map. This is the chain morphism from `P` to
the chain complex concentrated at 0 by the trivial representation `k` used to show `P` is a
projective resolution of `k`. It sends `x : k[G]` to the sum of its coefficients. -/
@[simps!]
noncomputable def resolution.π (g : G) :
    (chainComplexFunctor k g).obj (leftRegular k G) ⟶
      (ChainComplex.single₀ (Rep k G)).obj (trivial k G k) :=
  (((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv _).symm
    ⟨leftRegularHom _ 1, (leftRegularHomEquiv _).injective <| by simp [leftRegularHomEquiv]⟩

lemma resolution_quasiIso (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    QuasiIso (resolution.π k g) where
  quasiIsoAt m := by
    induction m with
    | zero =>
      simp only [resolution.π]
      rw [ChainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros' _ rfl rfl rfl]
      constructor
      · apply (Action.forget (ModuleCat k) _).reflects_exact_of_faithful
        simpa [ShortComplex.moduleCat_exact_iff_range_eq_ker,
          HomologicalComplex.alternatingConst, ChainComplex.toSingle₀Equiv] using
          leftRegular.range_applyAsHom_sub_eq_ker_linearCombination k g hg
      · rw [Rep.epi_iff_surjective]
        intro x
        use single 1 x
        simp [ChainComplex.toSingle₀Equiv]
    | succ m _ =>
      rw [quasiIsoAt_iff_exactAt' (hL := ChainComplex.exactAt_succ_single_obj ..),
          HomologicalComplex.exactAt_iff' _ (m + 2) (m + 1) m (by simp) (by simp)]
      apply (Action.forget (ModuleCat k) _).reflects_exact_of_faithful
      rw [ShortComplex.moduleCat_exact_iff_range_eq_ker]
      by_cases hm : Odd (m + 1)
      · simpa [if_pos (Nat.even_add_one.2 (Nat.not_even_iff_odd.2 hm)),
          if_neg (Nat.not_even_iff_odd.2 hm)]
          using leftRegular.range_norm_eq_ker_applyAsHom_sub k g hg
      · simpa [ShortComplex.moduleCat_exact_iff_range_eq_ker, if_pos (Nat.not_odd_iff_even.1 hm),
          if_neg (Nat.not_even_iff_odd.2 <| Nat.odd_add_one.2 hm)]
        using leftRegular.range_applyAsHom_sub_eq_ker_norm k g hg

/-- Given a finite cyclic group `G` generated by `g : G`, this is the projective resolution of `k`
as a trivial `k`-linear `G`-representation given by periodic complex
`... ⟶ k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] --N--> k[G] --(ρ(g) - 𝟙)--> k[G] ⟶ 0` where `ρ` is
the left regular representation and `N` is the norm map. -/
@[simps]
noncomputable def resolution (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    ProjectiveResolution (trivial k G k) where
  complex := (FiniteCyclicGroup.chainComplexFunctor k g).obj (leftRegular k G)
  projective _ := inferInstanceAs <| Projective (leftRegular k G)
  π := FiniteCyclicGroup.resolution.π k g
  quasiIso := resolution_quasiIso k g hg

end Rep.FiniteCyclicGroup
